\begin{tabbing}
es{-}first{-}at{-}since(${\it es}$;$i$;$e$;$e$.$R$($e$);$e$.$P$($e$))
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=loc($e$) = $i$\+
\\[0ex]\& $P$($e$) \& ($\neg$$R$($e$))
\\[0ex]\& ($\forall$${\it e'}$$<$$e$. $P$(${\it e'}$) $\Rightarrow$ ($\exists$${\it e''}$:E. (${\it e'}$ $\leq$loc ${\it e''}$  \& (${\it e''}$ $<$loc $e$) \& $R$(${\it e''}$))))
\-
\end{tabbing}